@Article{ErasSantSantVija:2015:ApBaUM,
               author = "Eras, Eduardo Rohde and Santos, Luciana Brasil Rebelo dos and 
                         Santiago J{\'u}nior, Valdivino Alexandre de and Vijaykumar, 
                         Nandamudi Lankalapalli",
          affiliation = "{} and {} and {Instituto Nacional de Pesquisas Espaciais (INPE)} 
                         and {Instituto Nacional de Pesquisas Espaciais (INPE)}",
                title = "Towards a wide acceptance of formal methods to the design of 
                         safety critical software: an approach based on UML and model 
                         checking",
              journal = "Lecture Notes in Computer Science",
                 year = "2015",
               volume = "9158",
                pages = "612--627",
                 note = "{Setores de Atividade: Pesquisa e desenvolvimento 
                         cient{\'{\i}}fico.}",
             keywords = "Model Checking, UML, Formal Methods, Formal Verification.",
             abstract = "The Unified Modeling Language (UML) is widely used to model 
                         systems for object oriented and/or embedded software development, 
                         specially by means of its several behavioral diagrams which can 
                         provide different points of view of the same software scenario. 
                         Model Checking is a formal verification method which has been 
                         receiving much attention from the academic community. However, in 
                         general, practitioners still avoid using Model Checking in their 
                         projects due to several reasons. Based on these facts, we present 
                         in this paper a significant improvement of a tool that we have 
                         developed which aims to translate several UML behavioral diagrams 
                         (sequence, activity, and state machine) into Transition Systems to 
                         support software Model Checking. With all the changes, we have 
                         applied our tool to a real space software product which is under 
                         development for a stratospheric balloon project to show how 
                         feasible is our approach in practice.",
                 issn = "0302-9743",
                label = "lattes: 5039690360728170 3 ErasSantSantVija:2015:ApBaUM",
             language = "en",
           targetfile = "eras_towards.pdf",
                  url = "http://link.springer.com/chapter/10.1007%2F978-3-319-21410-8_47",
        urlaccessdate = "02 maio 2024"
}